T:Type, f:(TT), L:(T List), x, y, z:T.
z=f*(x) via [y / L]
 {z = y
 & ((0 < ||L||)  (y = f(hd(L)) & ((y = hd(L))) & hd(L)=f*(x) via L))
 & (((0 < ||L||))  (x = y))} 

latex

Definitions

type List, Type, t  T, s = t, x:AB(x), x:A  B(x), P & Q, P  Q, x:A. B(x), P  Q, a < b, Void, False, A, ||as||, n+m, {i..j}, #$n, [], A  B, , , -n, , l[i], f(a), {x:A| B(x)} , i  j < k, [car / cdr], A List, P  Q, hd(l), i <z j, i z j, last(L), {T}, y=f*(x) via L, n - m, i  j , tl(l), s ~ t, True, T, SQType(T), left + right, P  Q, Dec(P), Atom, , b, x,y:A//B(x;y), x:A. B(x), b | a, a ~ b, |p|, a  b, a <p b, |g|, a < b, A c B, x f y, |r|, xL. P(x), (xL.P(x)), Unit,

Lemmas

decidable int equal, guard wf, length cons, nat wf, le wf, true wf, squash wf, iff wf, rev implies wf, select cons tl, non neg length, length wf1, int seg wf, select wf, not wf, member wf, length wf2